/*  Novelties: A visual novel programming language based on JavaFX
    Copyright (C) 2008  Hao Xu

    This program is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program.  If not, see <http://www.gnu.org/licenses/>.
 * /
/*
 * Literal.fx
 *
 * Created on Apr 13, 2008, 3:59:36 PM
 */

package avgengine.pred;

/**
 * @author ertri
 */

class Literal {
    attribute sign:int;
    attribute p: Predicate;
    attribute params: Term*;
    operation unify(l:Literal): Substitution;
    operation unifyTerm(t1:Term, t2:Term, sub:Substitution):boolean;
    operation unifyTerms(t1:Term*, t2:Term*, sub:Substitution):boolean;
    operation computeTerm(t1:Term):Term;
    operation fv(lits:Literal*):Variable*;
}
attribute Literal.sign = 1;
operation Literal.unify(l) {
    var sub = Substitution{};
    if(((l.sign>=0 and sign>=0) or (l.sign<0 and sign<0)) and l.p.n == p.n) {
        if(unifyTerms(l.params,params,sub)) {
            return sub;}}
    
    return null;
}
operation Literal.unifyTerm(t1:Term, t2:Term, sub:Substitution):boolean {
    if(t1 instanceof Variable) {
        sub.add((Variable)t1, t2);
        return true;
    } else if(t2 instanceof Variable) {
        sub.add((Variable)t2, t1);
        return true;
    } else {
        if(((FunctionTerm)t1).f.n == ((FunctionTerm)t2).f.n) {
            if(unifyTerms(((FunctionTerm)t1).params,((FunctionTerm)t2).params,sub)) {
                return true;}}
    }
    return false;
}
operation Literal.unifyTerms(t1:Term*, t2:Term*, sub:Substitution):boolean {
    if(sizeof t1 == sizeof t2) {
        if(sizeof t1 == 0) {
            return true;}
        
        var v1 = t1[0];
        var v2 = t2[0];
        if(not unifyTerm(v1, v2,sub)) {
            return false;}
        return unifyTerms(
        sub.subTerms(t1[n | indexof n > 0]),
        sub.subTerms(t2[n | indexof n>0]),
        sub
        );
    }
    return false;
    
}

operation Literal.fv(lits) {
    var fv = [];
    for(i in params) {
        fv = i.fv(fv);
    }
    for(l in lits) {
        for(i in l.params) {
            fv = i.fv(fv);
        }
    }
    return fv;
}
class Proposition extends Predicate, Literal {
    
}


trigger on new  Proposition {
    this.p = this;
    this.arity = 0;
    this.sign = 1;
}
